『Explaining Relaxed Memory Models with Program Transformations』
概要 弱いメモリモデルは並行プログラムの動作を決定する。弱メモリモデルは、ハードウェアやコンパイラが実行する並べ替えの観点から理解されることが多いが、その形式的な定義は、一般的に、公理的または操作的な、非常に異なるスタイルで与えられている。本論文では、既存のメモリモデルの弱い振る舞いが、どの程度まで並び替えや他のプログラム変換の観点から完全に説明できるかを調査する。我々は、TSOが逐次一貫性に対する2つの局所変換の集合と等価であることを証明するが、非マルチコピー原子モデル（C11、Power、ARMなど）は逐次一貫性に対する局所変換では説明できない。次に、基本的な非マルチコピーアトミックモデルに対する変換は、Powerの（大きな断片的な）緩和された振る舞いを説明するが、ARMの緩和された振る舞いは同様の方法では説明できないことを示す。我々の肯定的な結果は、高級言語からTSOやPowerへのコンパイル証明の正しさを単純化するために利用できる。 Release Consistency (RC)
メモリ操作をリリースとアクワイアに分けて扱い、特定の順序で操作が観測されることを保証します。
Weak Consistency (WC)
同じくリリースとアクワイアに基づいており、通常のメモリ操作の順序に関する制約を緩和します。
Total Store Order (TSO)
書き込み操作がプロセッサのキャッシュに一時的にバッファされることを許し、読み取り操作が書き込み操作に先行して実行される可能性を提供します。